摘要 :
Time Petri nets (TPNs) are a popular Petri net model for specification and verification of real-time systems. A fundamental and most widely applied method for analyzing Petri nets is reachability analysis. The existing technique f...
展开
Time Petri nets (TPNs) are a popular Petri net model for specification and verification of real-time systems. A fundamental and most widely applied method for analyzing Petri nets is reachability analysis. The existing technique for reachability analysis of TPNs, however, is not suitable for timing property verification because one cannot derive end-to-end delay in task execution, an important issue for time-critical systems, from the reachability tree constructed using the technique. In this paper, we present a new reachability based analysis technique for TPNs for timing property analysis and verification that effectively addresses the problem. Our technique is based on a concept called clock-stamped state class (CS-class). With the reachability tree generated based on CS-classes, we can directly compute the end-to-end time delay in task execution. Moreover, a CS-class can be uniquely mapped to a traditional state class based on which the conventional reachability tree is constructed. Therefore, our CS-class-based analysis technique is more general than the existing technique. We show how to apply this technique to timing property verification of the TPN model of a command and control (C2) system.
收起
摘要 :
This paper introduces compositional time Petri net (CTPN) models. A CTPN is a modularized time Petri net (TPN), which is composed of components and connectors. The paper also proposes a set of component-level reduction rules for T...
展开
This paper introduces compositional time Petri net (CTPN) models. A CTPN is a modularized time Petri net (TPN), which is composed of components and connectors. The paper also proposes a set of component-level reduction rules for TPNs. Each of these reduction rules transforms a TPN component to a very simple one while maintaining the net's external observable timing properties. Consequently, the proposed method works at a coarse level rather than at an individual transition level. Therefore, one requires significantly fewer applications to reduce the size of the TPN under analysis than those existing ones for TPNs. The use and benefits of CTPNs and reduction rules are illustrated by modeling and analyzing the response time of a command and control system to its external arriving messages.
收起
摘要 :
This paper presents a signal inversion technique in nondestructive evaluation (NDE) application for defect profile reconstruction using the element-free galerkin (EFG) method and state space search. The advantage of EFG method is...
展开
This paper presents a signal inversion technique in nondestructive evaluation (NDE) application for defect profile reconstruction using the element-free galerkin (EFG) method and state space search. The advantage of EFG method is that it relies only on a set of nodes, instead of a complex mesh to discretize the solution domain. In the inversion procedure, remeshing is avoided to increase the efficiency and accuracy of the solution, which is a major advantage over the traditional finite-element method (FEM). The iterative state space search method using the tree structure is developed for implementing the defect updating scheme. Preliminary results are presented for validation. The robustness of the technique has been shown on noisy signals.
收起
